\documentclass[a4paper]{article}

\usepackage[spanish]{babel}
\usepackage[latin1]{inputenc}
\usepackage{bbm}
\usepackage{framed}
\input{macrosAlgo1}

\newcommand{\comen}[2]{
\begin{framed}	
\noindent \textsf{#1:} #2
\end{framed}
}



\begin{document}

\materia{Algoritmos y Estructura de Datos I}
\cuatrimestre{1}
\anio{2012}

\fecha{30 de Marzo de 2012}

\nombre{\LARGE TPE OJOTA (Organizaci\'on de Juegos Ol\'impicos Tp de Algoritmos 1) v1.0}

\titulotp


\section{Tipos}

\input{tipos/tipos.tex}

\section{Atleta}
\input{tipos/atleta.tex}

\textbf{1.}
\begin{problema}{entrenarNuevoDeporte}{a: Atleta, d: Deporte, c: \ent}{}
\requiere[capacidadEnRango]{0 \leq c \leq 100}
\modifica{a}
\asegura[nombre]{nombre(a)==nombre(pre(a))}
\asegura[sexo]{sexo(a)==sexo(pre(a))}
\asegura[a\~{n}oNacimiento]{{a\~{n}oNacimiento}(a)=={a\~{n}oNacimiento}(pre(a))}
\asegura[nacionalidad]{nacionalidad(a)==nacionalidad(pre(a))}
\asegura[ciaNumber]{ciaNumber(a)==ciaNumber(pre(a))}
\asegura[noRepetirDeportes]{if$ $d \in deportes(pre(a))$ $then $ $deportes(pre(a))==deportes(a)\\$ $else$ $mismos(deportes(a), cons(d, deportes(pre(a)))}
\asegura[capacidad]{capacidad(a, d)==if$ $d \in deportes(pre(a))$ $then$ $capacidad(pre(a), d)$ $else$ $c}
\asegura {ordenada (deportes(a))}
\asegura {(\forall ds \leftarrow deportes(a), d \neq ds) capacidad (a,ds) == capacidad (pre(a),ds))}
\end{problema}



\section{Competencia}

\input{tipos/competencia.tex}

\textbf{2.}
\begin{problema}{finalizarCompetencia}{c: Competencia, posiciones: [Atleta], control: [(Atleta, \bool)]}{}
\requiere{incluida(posiciones,participantes(c))}
\requiere{incluida([prm(x)|x \leftarrow  control],participantes(c))}
\modifica{c}
\asegura{categoria(c)==categoria(pre(c))}
\asegura{mismos(participantes(c), participantes(pre(c)))}
\asegura{finalizada(c)==True}
\asegura{ranking(c)==posiciones}
\asegura{mismos(lesTocoControlAntiDoping(c),[prm(cs)|cs \leftarrow control])}
\asegura{(\forall at \leftarrow control) leDioPositivo(c,prm (at)) == sgd (at)}
\end{problema}

\textbf{3.}
\begin{problema}{linfordChristie}{c: Competencia, a: Atleta}{}
\requiere[]{finalizada(c)==false}
\requiere[]{a\in participantes(c)}
\modifica{c}
\asegura[]{mismos (participantes(pre(c)),a:participantes(c))}
\asegura[]{categoria(c)==categoria(pre(c))}
\asegura[]{finalizada(c)==finalizada(pre(c))}
\end{problema}

\textbf{4.}
\begin{problema}{gananLosMasCapaces}{c: Competencia}{Bool}{}
\requiere[]{finalizada(c)==true}
\asegura[]{result==ordenadaPorCapacidad(ranking(c),prm(categoria(c)))}
\end{problema}

\textbf{5.}
\begin{problema}{sancionarTramposos}{c: Competencia}{}
\requiere[competenciaFinalizada]{finalizada(c)==true}
\modifica{c}
\asegura[mismaCategoria]{categoria(c)==categoria(pre(c))}
\asegura[mismosParticipantes]{mismos(participantes(c),participantes(pre(c)))}
\asegura[yaFinalizada]{finalizada(c)==finalizada(pre(c))}
\asegura[controlados]{mismos(lesTocoControlAntiDoping(c)==lesTocoControlAntiDoping(pre(c)))}
\asegura[lesDioPositivo]{(\forall a \leftarrow lesTocoControlAntiDoping(c)) lesDioPositivo(c, a)==lesDioPositivo(pre(c), a)}
\asegura[eliminarDelRanking]{mismos(([x|x\leftarrow lesTocoControlAntiDoping(c), leDioPositivo(c, x)] ++ ranking(c)), \newline ranking(pre(c)))}
\asegura[reordenada]{ordenRelativo(ranking(c), ranking(pre(c)))}
\end{problema}

\textbf{6.}
\begin{problema}{clasificoTarde}{c:Competencia,a:Atleta}{}
\requiere{finalizada(c)==false}
\requiere{a\notin participantes(c)}
\requiere{prm(categoria(c))\in deportes(a)}
\requiere{sgd(categoria(c))==sexo(a)}
\modifica{c}
\asegura{mismos (participantes(c),a:participantes(pre(c))}
\asegura{categoria(c)==categoria(pre(c))}
\asegura{finalizada(c)==finalizada(pre(c))}
\end{problema}

\section{JJOO}
\input{tipos/jjoo.tex}

\textbf{7.}
\begin{problema}{dePaseo}{j: JJOO}{[Atleta]} 
\requiere[queHayaParticipantes]{|[x|x\leftarrow participantes(j)]|>0}
\asegura[losQueNoEstan]{mismos(result, losQueNoParticipan(j)}
\end{problema}

\textbf{8.}
\begin{problema}{medallero}{j: JJOO}{[(Pais,[\ent])]}
\asegura{sinRepetidos(result)}
\asegura{estaOrdenadaSegunMedallero(result)}%falta arreglar
\asegura{(\forall p2 \selec [prm(p1)|p1 \selec result]) p2 \in (paisesOro(j)++paisesPlata(j)++paisesBronce(j))}
\asegura{(\forall p2 \selec (paisesOro(j)++paisesPlata(j)++paisesBronce(j)) p2 \in [prm(r)|r\leftarrow result]}
\asegura{(\forall r \selec [(prm(p1),sgd(p1)) | p1 \selec result]) sgd(r)==cantMedallasPorPais(prm(r))}
\end{problema}

\textbf{9.}
\begin{problema}{boicotPorDisciplina}{j: JJOO, cat: (Deporte, Sexo), p: Pais}{\ent}{}
\requiere[categoriaExistente]{}{$|[c|$c\leftarrow competencias(j), categoria(c)==cat]|>0}
\asegura[noCambiaA\~{n}o]{a\~{n}o(j)==a\~{n}o(pre(j)}
\asegura[noCambianAtletas]{mismos(atletas(j), atletas(pre(j)))}
\asegura[noCambiaCantDias]{cantDias(j)==cantDias(pre(j))}
\asegura[noCambiaJornadaActual]{jornadaActual(j)==jornadaActual(pre(j))}
\asegura[noCambianAtletas]{mismos(atletas(j), atletas(pre(j))}
\asegura[lasDemasNoCambian]{(\forall d \leftarrow [1..cantDias(j)])\\ 
mismos([x|x\leftarrow cronograma(j,d), categoria(x) \neq cat], [x|x\leftarrow cronograma(pre(j),d), categoria(x) \neq cat])}
\asegura[existeEnElMismoDia]{(\exists c\leftarrow cronograma(j, [d|d\leftarrow [1..cantDias(j)], l\leftarrow cronograma(pre(j), d), (\exists b \in l \wedge categoria(b)==cat)]_{0}) categoria(c)==cat}
\asegura[soloCambianParticipantes]{igualSalvoParticipantes([x|x \leftarrow competencias(j), categoria(x) == cat]_{0}, [x|x \leftarrow competencias(pre(j)), categoria(x) == cat]_{0})}
\asegura[quitarParticipantes]{mismos([x|c\leftarrow competencias(j), x\leftarrow participantes(c), categoria(c)==cat],
[y|b\leftarrow competencias(pre(j)), y\leftarrow participantes(b), categoria(b)==cat \wedge nacionalidad(y)\neq p])}
\asegura[numeroRetirados]{result==|[x|c\leftarrow competencias(pre(j)), x\leftarrow participantes(c), \\categoria(c)==cat \wedge nacionalidad(x)==p]|}

\end{problema}

\textbf{10.}
\begin{problema}{losMasFracasados}{j:JJOO,p:Pais}{[Atleta]}{}
\asegura{mismos(result,[a|a\leftarrow losQueMasParticiparon(j,p), |compEnTop3(j,a)|==0])}
\end{problema}

\textbf{11.}
\begin{problema}{liuSong}{j:JJOO, a:Atleta, p:Pais}{[Atleta]}{}
\requiere{a \in atletas(j)}
\requiere{\neg ( \exists a1 \leftarrow atletas (j)), igualSalvoPais (a,a1,p)}
\modifica {j}
\asegura {a\~{n}o(j)==a\~{n}o(pre(j))}
\asegura {cantDias(j)==cantDias(pre(j))}
\asegura {cronograma(j,d)==cronograma(pre(j,d))}
\asegura {jornadaActual(j)==jornadaActual(pre(j))}
\asegura {|atletas(j)|==|atletas(pre(j))|}
\asegura{(\forall d \leftarrow [1..cantDias(j)], c \leftarrow cronograma (j,d), at \leftarrow participantes (c), at == a, nacionalidad (at) == p)}
\asegura {(\forall a2 \leftarrow atletas(pre(j)), a2 \neq a) (\exists a3 \leftarrow atletas(j),a2==a3) \wedge igualSalvoLiuSong (j,a2)}
\asegura {(\forall a2 \leftarrow atletas(pre(j)), a2 == a) (\exists a3 \leftarrow atletas(j), igualSalvoPais(a2,a3,p)}
\end{problema}

\textbf{12.}
\begin{problema}{stevenBradbury}{j: JJOO}{Atleta}
\requiere{|ganaronOro(j)| > 0}
\asegura{result \in ganaronOro(j)}
\asegura{(\nexists a \selec ganaronOro(j), a \neq result , c \selec capacidadesDeportesGanoOro(a,j))
\newline c \leq minimo(capacidadesDeportesGanoOro(result,j))}%corregido%
\end{problema}

\textbf{13.}
\begin{problema}{uyOrdenadoAsiHayUnPatron}{j: JJOO}{Bool}{}
\asegura[]{result==hayPatron(listaDeMejores(j))}
\end{problema}

\textbf{14.}
\begin{problema}{sequiaOlimpica}{j:JJOO}{[Pais]}{}
\requiere{jornadaActual(j)>1}
\asegura{mismos(result,[p|p\leftarrow paisesQueParticiparon(j), \forall q \leftarrow paisesQueparticiparon(j), q\neq p, \\sequiaDelPais(j,p) \geq  sequiaDelPais(j,q)])}
\end{problema}

\textbf{15.}
\begin{problema}{transcurrirDia}{j: JJOO}{}
\requiere{jornadaActual(j) \neq cantDias(j)}%corregido%
\modifica{j}
\asegura{a\~{n}o(j)==a\~{n}o(pre(j))}
\asegura{cantdias(j)==cantDias(pre(j))}
\asegura{jornadaActual(j)==jornadaActual(pre(j))+1}
\asegura{(\forall c \selec cronograma(j,jornadaActual(j))\newline finalizada(c) \wedge rankingOrdenadoPorCapacidad(ranking(c), sgd(categoria(c))) \wedge antiDopingAUnUnico(c)}%corregido%
\asegura{leDioPositivo5PorCiento(cronograma(j ,jornadaActual(j)))}
\asegura{(\forall dia \selec [1..cantDias(j)], dia \neq jornadaActual(j)) cronograma(j,dia) == cronograma(pre(j),dia)}%corregido agregado%
\end{problema}

\textbf{16.}
\begin{problema}{deportesNoOlimpicos}{j:JJOO}{[Deporte]}{}
\asegura{mismos(result,depNoOlimpicos(j))}
\end{problema}
%faltan los aux%

\textbf{17.}
\begin{problema}{atletaProdigio}{js:[JJOO],cat:(Deporte,Sexo)}{Atleta}{}
\requiere{js\neq []}
\requiere{((\exists j\leftarrow js, d\leftarrow [1..cantDias(j)]) \exists c\leftarrow cronograma(j,d), categoria(c)==cat)}
\requiere{|ganadoresOroEnEstaCategoria(js,cat)|>0}
\asegura{result\in ganadoresMenorEdad(js,cat)}
\end{problema}
\section{Auxiliares}

\input{auxiliaresTipos.tex}

\aux{antiDopingAUnUnico}{c: Competencia}{Bool}{|lesTocoControlAntiDoping(c)|\leq 1}%corregido%
\aux {atletasDelPais}{j:JJOO,p:Pais}{[Atleta]}{[a|a\leftarrow atletas(j), nacionalidad(a)==p]}
\aux{atletasOroDiario}{j: JJOO, dia: \ent}{[Atleta]}{[cab(ranking(c))|c \selec cronograma(j,dia),finalizada(c),\\|ranking(c)|>0]}%corregido pero nose poner nueva linea%
\aux{cantMedallasDeOroPorDia}{p: Pais, dia: \ent, j: JJOO}{\ent}{cuenta(p,paisesOroDiario(j,dia))}
\aux{cantMedallasPorPais}{p: Pais, j: JJOO}{[\ent]}{\newline[cuenta(p,paisesOro(j)),cuenta(p,paisesPlata(j)),cuenta(p,paisesBronce(j))]}
\aux{capacidadesDeportesGanoOro}{a: Atleta, j: JJOO}{[\ent]}{[capacidad(a,d) |c \selec competencias(j),
\newline  finalizada(c), |ranking(c)|>0, d \selec prm(categoria(c)), d \in deportes(a), cab(ranking(c)) == a]}
\aux {compEnTop3}{j:JJOO,a:Atleta}{[Competencia]}{[c|d\leftarrow[1..jornadaActual(j)),c\leftarrow cronograma(j,d),\\a\in top3Medallas(j,c)}
\aux{compParticipadas}{j:JJOO,a:Atleta}{[Competencia]}{[c|d\leftarrow [1..jornadaActual(j)),c\leftarrow cronograma(j,d),\\a\in participantes(c)]}
\aux{depNoOlimpicos}{j:JJOO}{[Deporte]}{[d|d\leftarrow todosLosDeportes(j), (d\in deportesOlimpicos(j))==False]}
\aux{depOlimpicos}{j:JJOO}{[Deporte]}{[prm(categoria(c))|d\leftarrow [1..cantDias(j)], c\leftarrow cronograma(j,d)]}
%ver si no se indefine enEsteDiaGanoOro%
\aux{enEsteDiaGanoOro}{j:JJOO,d:\ent,p:Pais}{\ent}{\beta((\exists c\leftarrow cronograma(j,d),|ranking(c)|\geq 1)\\( \exists a\leftarrow ranking(c), a==cab(ranking(c)))nacionalidad(a)==p)}
\aux{esGrandeYEstaOrdenadoLexicograficamente}{x:(Pais,[\ent]), l:[T]}{Bool}{(\forall y \in l, y \neq x)\\ sgd(x)\geq sgd(y) \wedge prim(x) < prim(y)}
\aux{esMasGrandeQueTodos}{x:T, l:[T]}{Bool}{(\forall y \in l, y \neq x) x>y}
\aux{estaOrdenadaSegunMedallero}{l:[(Pais,[\ent])]}{Bool}{(\forall i, j \leftarrow [0..|l|) if$ $cab(sgd(l_{i})) \geq cab(sgd(l_{j})) \wedge i < j$ $then$ $True$ $else$ $if$ $cab(sgd(l_{i})) == cab(sgd(l_{j})) \wedge indice(sgd(l_{i}), 1) > indice(sgd(l_{j}), 1) \wedge i < j  $ $then$ $True$ $
else$ $if$ $\\cab(sgd(l_{i})) == cab(sgd(l_{j})) \wedge indice(sgd(l_{i}), 1) == indice(sgd(l_{j}), 1) \wedge indice(sgd(l_{i}), 2) > indice(sgd(l_{j}), 2) \wedge i < j $ $then$ $True$ $
else$ $false}
\aux{ganadoresMenorEdad}{js:[JJOO],cat:(Deporte,Sexo)}{[Atleta]}{[a1|j1\leftarrow js, d1\leftarrow [1..cantDias(j1)],\\ c1\leftarrow cronograma(j1,d1),|ranking(c1)|>0,  categoria(c1)==cat, a1==cab(ranking(c1)),\\(\forall j2\leftarrow js, d2\leftarrow [1..cantDias(j)], c2\leftarrow cronograma(j2,d2),|ranking(c2)|>0, categoria(c2)==cat,\\a2\leftarrow cab(ranking(c2)) (a\~{n}o(j1)-a\~{n}oNacimiento(a1)) \leq (a\~{n}o(j2)-a\~{n}oNacimiento(a2))]}
\aux{ganadoresOroEnEstaCategoria}{js:[JJOO],cat:(Deporte,Sexo)}{[Atleta]}{\newline[cab(ranking(c))|j \selec js, d \selec [1..cantDias(j)],c \selec cronograma(j,d),|ranking(c)|>0,finalizada(c),\\categoria(c)==cat]}
\aux{ganaronBronce}{j: JJOO}{[Atleta]}{\newline[indice(x,2)|x\selec rankingCompetencias(j),|rankingCompetencias(j)| \geq 3]}%corregido revisar%
\aux{ganaronOro}{j: JJOO}{[Atleta]}{\newline[cab(x)|x\selec rankingCompetencias(j),|rankingCompetencias(j)| \geq 1]}%corregido revisar%
\aux{ganaronPlata}{j: JJOO}{[Atleta]}{\newline[indice(x,1)|x\selec rankingCompetencias(j),|rankingCompetencias(j)| \geq 2]}%corregido revisar%
\aux{hayPatron}{l:[T]}{Bool}{(\forall i\leftarrow [0..|l|-cabeza(cola(obtenerIndices(l_{0}, l))) indice(l, i) ==\\ indice(l, cabeza(cola(obtenerIndices(l_{0}, l)+i)}
\aux {igualSalvoLiuSong}{j:JJOO, a2: atleta}{Bool}{\forall d \leftarrow [1...cantDias(j)], mismos ([a2| c \leftarrow cronograma (j,d),\\ a2 \in participantes (c )],[a2| c \leftarrow cronograma(pre(j),d), a2 \in participantes(c )])}
\aux {igualSalvoPais}{x1,x2:atleta, p: pais}{Bool}{nombre(x1)==nombre(x2)\wedge sexo(x1)==sexo(x2) \wedge \\a\~{n}oNacimiento(x1)==a\~{n}oNacimiento(x2)\wedge nacionalidad(x2)== p \wedge ciaNumber(x1)==ciaNumber(x2)\wedge \\deportes(x1)==deportes(x2) \wedge  (\forall d1 \leftarrow deportes(x1), d2 \leftarrow deportes (x2))(capacidad(x1,d1)==capacidad(x2,d2))}
\aux{igualSalvoParticipantes}{c, d: Competencia}{Bool}{(categoria(c)==categoria(d) \wedge finalizada(c)==finalizada(d))}
\aux{leDioPositivo5PorCiento}{c: [Competencia]}{Bool}{|[a | c1 \selec c, a \selec lesTocoControlAntiDoping(c1), \\leDioPositivo(c1,a)]| \leq |[[a | c1 \selec c, a \selec lesTocoControlAntiDoping(c1)]| * 0.05}%corregido%
\aux{listaDeMejores}{j:JJOO}{[Pais]}{[x|d\leftarrow[1..jornadaActual(j)), x\leftarrow mejorPorDia(d,j)]}
\aux{losQueMasParticiparon}{j:JJOO,p:Pais}{[Atleta]}{[a|a\leftarrow atletasDelPais(j,p),(\forall b\leftarrow atletasDelPais(j,p))\\ |compParticipadas(j,a)|\geq |compParticipadas(j,b)|]}
\aux{losQueNoParticipan}{j:JJOO}{[Atleta]}{[x|x\leftarrow atletas(j), x \notin losQueParticipan(j)]}
\aux{losQueParticipan}{j:JJOO}{[Atleta]}{[x|c\leftarrow competencias(j), x\leftarrow participantes(c)]}
\aux{maximo2}{l:[(p: Pais,d: \ent)]}{Pais}{[prm(x)| x\leftarrow l, esMasGrandeQueTodos(sgd(x), l) \\\vee esGrandeYEstaOrdenadoLexicograficamente(x, l)]}
\aux{medallasEnLosJuegos}{j:JJOO,p:Pais}{[\ent]}{[z|d\leftarrow [1..jornadaActual(j)), z==enEsteDiaGanoOro(j,d,p)]}
\aux{medallasPorDiaPorPais}{d:\ent , j:JJOO}{[(Pais,\ent)]}{[(p, cantMedallasDeOroPorDia(p, d, j))| a\leftarrow atletas(j), \\p\leftarrow nacionalidad(a)]}
\aux{mejorPorDia}{d:\ent , j:JJOO}{Pais}{[x|x\leftarrow maximo2(medallasPorDiaPorPais(d, j)]_{o}}
\aux{minimo}{l:[\ent]}{\ent}{cab[l_i | i \selec [0..|l|), \forall j \selec [0..|l|), l_i \leq l_j]}
\aux{obtenerIndice}{l:[T], a: T}{\ent}{[i|i\leftarrow [0..|l|), li==a]_{0}}
\aux{obtenerIndices}{l:[T],a:T}{[\ent]}{[i|i\leftarrow [0..|l|), li==a]}
\aux {ordenadaPorCapacidad}{L: [Atletas], d: deporte}{Bool}{(\forall x \in L, \forall i \leftarrow [0..|l|),\forall j \leftarrow [0..|l|) )$ $\\if$ $ capacidad(x_{i}, d) \geq capacidad(x_{j},d) $ $ \wedge$  $ i \leq j $ $then$ $ True $ $else$ $False}
\aux{ordenRelativo}{$l_{1}, l_{2}: [T]$}{Bool}{If$ $ l_{1}== [] $ $ then $ $ true $ $ else $ $ 
(\forall i \leftarrow [0..|l_{1}|), \forall  j \leftarrow [0..|l_{1}|)) $ $\\if$ $obtenerIndice(l_{2}, l_{i}) < obtenerIndice(l_{2}, l_{j})$ $\wedge  $ $i < j$ $then$ $true$ $ else $ $ false}
\aux{paisesOroDiario}{j: JJOO, dia: \ent}{[Pais]}{[nacionalidad(a)|a \selec atletasOroDiario(j,dia)]}
\aux{paisesOro}{j: JJOO}{[Pais]}{[nacionalidad(x)|x \selec ganaronOro(j)]}
\aux{paisesPlata}{j: JJOO}{[Pais]}{[nacionalidad(x)|x \selec ganaronPlata(j)]}
\aux{paisesBronce}{j: JJOO}{[Pais]}{[nacionalidad(x)|x \selec ganaronBronce(j)]}
\aux{paisesQueParticiparon}{j:JJOO}{Pais}{[p|d\leftarrow [1..jornadaActual(j)),c\leftarrow cronograma(j,d),\\a\leftarrow participantes(c),p==nacionalidad(a)]}
\aux{rankingCompetencias}{j: JJOO}{[[Atleta]]}{[ranking(c)|d \selec [1..cantDias(j)], c \selec cronograma(j, d),\\finalizada(c)]}
\aux{rankingOrdenadoPorCapacidad}{c: Competencia}{Bool}{(\forall i \selec [0..|ranking(c)|))\\ capacidad(ranking(c)_i,prm(categoria(c))) \geq capacidad(ranking(c)_{i+1},prm(categoria(c)))}
\aux{sequiaDelPais}{j:JJOO,p:Pais}{\ent}{|sequiaMasLarga (j,p)|}
\aux{sequiaMasLarga}{j:JJOO,p:Pais}{[\ent]}{\\cab[l_1|l_1 \leftarrow todasLasSequias(obtenerIndices(medallasEnLosJuegos(j,p),0)),\\ \forall l_2 \leftarrow todasLasSequias(obtenerIndices(medallasEnLosJuegos(j,p),0))) |l_1|\geq |l_2|]}
\aux{todasLasSequias}{l:[\ent]}{[[\ent]]}{[[a..b]|a,b\leftarrow l, incluida([a..b],l)]}
\aux{todosLosDeportes}{j:JJOO}{[Deporte]}{[d|a\leftarrow atletas(j), d\leftarrow deportes(a)]}
\aux{top3Medallas}{j:JJOO,c:Competencia}{[Atleta]}{[a|a\leftarrow atletas(j),d\leftarrow [1..jornadaActual(j)), \\c\in cronograma(j,d), if$ $|ranking(c)|>2$ $then$ $a\in sub(ranking(c),0,2)$ $else$ $a\in ranking(c)]}


\end{document}
